COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Notes on Heavy Duty Set Theory
C00013 ENDMK
C⊗;
Notes on Heavy Duty Set Theory


	"Heavy Duty Set Theory" (abbreviated HDST) is to be an
FOL axiomatization of set theory suitable for proving theorems
in various domains of mathematics, MTC, and artificial intelligence.
The object of the axiomatization is to make proofs as short as
possible and to get as close as possible to informal notation.
Therefore, it will have a large number of axioms.

Recommendations:

1. HDST will be like Kelley's system in containing both classes
and sets and also axiom schemata for comprehension and replacement.

2. There will be members of sets that are not sets, and the axioms
will have to be adjusted for this.  Numbers and S-expressions
will be sorts and will be axiomatized and identified with the
machine versions.
This may be incompatible with identifying numbers with certain sets.
An isomorphism with this set can be asserted if wanted.

3. apply(f,x) giving the value of f(x) will be present and suitably
axiomatized.  In order that apply can be a function in the logic
we will need an INDCONST UU which is the nominal value for undefined
quantities. *****I'm not quite sure of this.*****

4. Suitable sorts for sets, classes, and objects will be set up.

5. Can we make cons and the ordered pair former synonymous?
If we want the ordered tuple to satisfy reasonable axioms,
it should be made more like LISP.
For example, we should distinguish between ordered pairs
and tuples: Suppose we use (x.y) for the ordered pair
usually denoted by <x,y>.  We will then use λ for
the 0-tuple, and define the n+1-tuple by suitable instances of
<x1,x2,...,xn> = (x1.<x2,...,xn>).

6. We will distinguish two systems; those that don't involve modifications
to FOL and those that do.

7. If we can modify FOL, then the finite set former {a,b,d,e} should
be such that membership and subset relationships are immediate.
Thus "SET-OBVIOUSITY {b {d e}} ⊂ {{f d} a b} 7;", where 7 is f=e,
should work.  Richard points out that a collection of such results
can be obtained from taut by a suitable translation.

8. For ordered lists, inclusion relations should be obvious.
In general: what set-theoretic relations are obvious?

Here is an attempt to modify kelley.ax[ax,rww] to suit.  The current
version her reads into FOL.  The SETINDUCTION axiom is not correct.
Ordered triples have been omitted pending a notation change.  ⊗ and
EXP2 and EXP3 have been omitted.